Listar por autor 

Listar por autor "Martín Mateos, Francisco Jesús"                

Mostrando ítems 1-20 de 43

    • Ponencia
      Icon

      A Formal Proof of Dickson’s Lemma in ACL2 

      Martín Mateos, Francisco Jesús; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Ruiz Reina, José Luis (Springer, 2003)
      Dickson’s Lemma is the main result needed to prove the termination of Buchberger’s algorithm for computing Gr¨obner basis ...
    • Ponencia
      Icon

      A Formally Verified Prover for the ALC Description Logic 

      Alonso Jiménez, José Antonio; Borrego Díaz, Joaquín; Hidalgo Doblado, María José; Martín Mateos, Francisco Jesús; Ruiz Reina, José Luis (Springer, 2007)
      The Ontology Web Language (OWL) is a language used for the Semantic Web. OWL is based on Description Logics (DLs), a ...
    • Ponencia
      Icon

      A Generic Instantiation Tool and a Case Study: A Generic Multiset Theory. 

      Martín Mateos, Francisco Jesús; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Ruiz Reina, José Luis (University of Texas, 2002)
      In some cases, when we develop a formal theory in ACL2, it would be desirable that the definitions and theorems of the ...
    • Ponencia
      Icon

      A Theory About First-Order Terms in ACL2 

      Ruiz Reina, José Luis; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Martín Mateos, Francisco Jesús (University of Texas, 2002)
      We describe the development in ACL2 of a library of results about first-order terms. In particular, we present the ...
    • Ponencia
      Icon

      ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System 

      Martín Mateos, Francisco Jesús; Rubio, Julio; Ruiz Reina, José Luis (Springer, 2009)
      Kenzo is a Computer Algebra system devoted to Algebraic Topology, and written in the Common Lisp programming language. ...
    • Ponencia
      Icon

      Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials 

      Lambán Pardo, Laureano; Martín Mateos, Francisco Jesús; Rubio, Julio; Ruiz Reina, José Luis (Springer, 2011)
      In this paper we present a complete formalization, using the ACL2 theorem prover, of the Normalization Theorem, a result ...
    • Ponencia
      Icon

      Certified Symbolic Manipulation: Bivariate Simplicial Polynomials 

      Lambán Pardo, Laureano; Martín Mateos, Francisco Jesús; Rubio, Julio; Ruiz Reina, José Luis (ACM, 2013)
      Certified symbolic manipulation is an emerging new field where programs are accompanied by certificates that, suitably ...
    • Artículo
      Icon

      Constructing Formally Verified Reasoners for the ALC Description Logic 

      Hidalgo Doblado, María José; Alonso Jiménez, José Antonio; Martín Mateos, Francisco Jesús; Ruiz Reina, José Luis (Elsevier, 2008)
      Description Logics are a family of logics used to represent and reason about conceptual and terminological knowledge. ...
    • Trabajo Fin de Grado
    • Trabajo Fin de Grado
      Icon

      Desarrollo de una librería Haskell sobre árboles de decisión 

      García Sancho, Carlos (2021-12-02)
      A Decision Tree is a supervised learning technique used for prediction tasks, which stands out for being able to produce ...
    • Trabajo Fin de Grado
      Icon

      Desarrollo de una librería Haskell sobre códigos QR 

      Delgado Cruces, Javier (2021-06-18)
      QR codes are the most common way of storing and exchanging information. In this project they will be studied in order to create a Haskell package with necessary functions and data types to implement them.
    • Trabajo Fin de Grado
      Icon

      Desarrollo de una librería Haskell sobre redes neuronales 

      Ramírez de Arellano Marrero, Antonio (2020-06-01)
      Artificial Neural Networks are a computational model whose objective is to simulate the learning system of the human ...
    • Ponencia
      Icon

      Expert System to Real Time Control of Machining Processes 

      Martín Mateos, Francisco Jesús; González Valencia, Luis Carlos; Serrano Bello, Rafael (Springer, 2009)
      Industrial machining processes use automated milling machines. These machines are connected to a control device that ...
    • Artículo
      Icon

      Formal Correctness of a Quadratic Unification Algorithm 

      Ruiz Reina, José Luis; Martín Mateos, Francisco Jesús; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José (Springer, 2006)
      We present a case study using ACL2 [5] to verify a non-trivial algorithm that uses efficient data structures. The algorithm ...
    • Artículo
      Icon

      Formal proofs about rewriting using ACL2 

      Ruiz Reina, José Luis; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Martín Mateos, Francisco Jesús (Springer, 2002)
      We present an application of the ACL2 theorem prover to reason about rewrite systems theory. We describe the formalization ...
    • Ponencia
      Icon

      Formal Reasoning about Efficient Data Structures: A Case Study in ACL2 

      Ruiz Reina, José Luis; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Martín Mateos, Francisco Jesús (Springer, 2003)
      We describe in this paper the formal verification, using the ACL2 system, of a syntactic unification algorithm where terms ...
    • Artículo
      Icon

      Formal verification of a generic framework to synthesize SAT-provers 

      Martín Mateos, Francisco Jesús; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Ruiz Reina, José Luis (Springer, 2004)
      We present in this paper an application of the ACL2 system to generate and reason about propositional satis ability ...
    • Ponencia
      Icon

      Formal Verification of Molecular Computational Models in ACL2: A Case Study 

      Martín Mateos, Francisco Jesús; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Ruiz Reina, José Luis (Springer, 2003)
      Theorem proving is a classical AI problem with a broad range of applications. Since its complexity is exponential in the ...
    • Tesis Doctoral
      Icon

      Formalización en Isar de la metalógica de primer orden 

      Serrano Suárez, Fabián Fernando (2012-06-12)
      El objetivo del trabajo es formalizar razonamiento complejo de forma legible por los humanos y procesable por las máquinas. ...
    • Artículo
      Icon

      Formalization of a normalization theorem in simplicial topology 

      Lambán Pardo, Laureano; Martín Mateos, Francisco Jesús; Rubio, Julio; Ruiz Reina, José Luis (Springer, 2012)
      In this paper we present a complete formalization of the Normalization Theorem, a result in Algebraic Simplicial Topology ...